Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Wir machen Logik 1. Stufe und hatten das gestern relativ gründlich, Syntax und Semantik durchgesprochen und Substitutionen.

Wir haben eine Logik, die über Individuen reden und Aussagen machen kann.

Und wir haben eine Sprache, die Zweiteilsprache hat, die Termsprache.

Das sind Objekte, die bedeuten Individuen. Und die Aussagensprache, die bedeutet, war oder falsch.

Im Prinzip kann man sich das vorstellen, dass wenn man die Terme als Bäume sich andenkt, dann sieht ja eine Formel oder eine Aussage so aus.

Und dann ist das so wie so ein Berg mit einer Eiskappe.

Hier oben leben und, nicht und für alle. Hier unten leben F und A und X.

Und an der Grenze leben P, Q, R und so was die Relationen.

Und das ist ein Berg, der ist nicht wie so ein Alpenberg, wo es hier unten irgendwo noch Schneefelder gibt.

Sondern das ist so ein bisschen wie Mount Fujiyama, wo es tatsächlich eine Grenze ist.

Da oben kann man dann die Ski stehen lassen und ab da kann man laufen, wenn man runterfährt.

So sind die hier aufgebaut, denn wenn man von oben kommt, sieht man für alle und nicht und so weiter.

Dann kommt man an diese Prädikate und die Prädikate haben als Argumente Terme und ab da ist Grün.

Gut. So, wir hatten freie und gebundene Variablen diskutiert.

Die können wir einfach und das ist das Tolle an sowas wie Logiksprache, die sind einfach induktiv definiert.

Das heißt, die kann man mit Baummethoden sehr gut behandeln.

Und wir hatten uns die Interpretationsfunktionen, Modelle und Evaluation, also die Wertberechnung, angeguckt.

Wertberechnung relativ kompliziert, für beide Teilsprachen eine eigene Rekursion.

Und das ist alles relativ straightforward. Variablen werden über die Variablenbelegung abgefackelt.

Für sowas wie Funktionen und Prädikate und Junktoren gehen wir einfach homomorph runter.

Wir berechnen die Werte der Argumente und wenden die Interpretation der Funktion oder des Prädikates darauf an.

Und interessant wird es beim Alquantor.

Beim Alquantor ist es nämlich so, dass wir auch den Wert des Rumpfes berechnen, aber mit einem ganzen Schwarm von erweiterten Variablenbelegungen.

Damit wir die hier an der Stelle erweitern können, haben wir ja auch diese zweiteilige Wertfunktion.

Einmal machen wir eine Interpretation, der ist stabil. Und die Variablenbelegung, wie auch der Name sagt, ist variabel, damit wir sie hier unten erweitern können.

Ziemlich trickreiche Sache.

So, das war Bedeutung. Dadurch können wir Folgerungen machen, alle solche Sachen.

Jetzt gehen wir in die Richtung Kalküle. Eine ganz wichtige Sache, die wir machen müssen, wenn wir über Kalküle in der Logik ersten Stufen reden, ist,

wir müssen mit gebundenen Variablen, mit all quantifizierten Variablen umgehen und mit existenzquantifizierten Variablen umgehen.

Die Standardlösung dazu sind Substitutionen. Substitutionen sind Dinge, die Variablen durch Terme ersetzen.

Und dabei gibt es eine ganze Menge Handwerkszeug.

Wie schreibt man die Biester auf? Wie wendet man die Biester an? Wie erweitert man sie? Was ist die... und so weiter.

Das haben wir alles ziemlich genau durchgesprochen. Und ich möchte Sie warnen, Substitutionen sind schwer.

Gucken Sie sich die Definitionen an, wenn Sie die Definitionen falsch haben, dann funktionieren die Sachen nicht, wie sie sollen.

Als ich angefangen habe zu promovieren, habe ich in einem Gebiet namens Unifikationstheorie angefangen.

Das war ein Gebiet, da waren Substitutionen schon im Wesentlichen 60 Jahre alt.

Ich bin auf meine erste Konferenz gefahren und ein Kollege von mir hat den Leuten mal beigebracht, wie man Substitutionen definieren muss.

Denn alle Resultate vorher in der Unifikationstheorie, die es seit etwa 15 Jahren gab, waren alle falsch.

Das war ihm irgendwann mal aufgefallen. Das heißt, wenn schlaue Leute falsche Definitionen nehmen, dann waren die Definitionen nicht so einfach.

Diese Sachen muss man aufpassen. Substitutionserweiterung, andere Stück Handwerkszeug.

Variablen einfangen. Bevor ich substituiere, muss ich sehen, dass ich diese Variablen aus dem Weg umbenahmse.

Denn sonst werden die Kalküle hinterher nicht zahnt. Und ähnliche Dinge.

Was wir weiterhin gemacht haben, ist, dass wir uns darauf vorbereiten, Soundness, also Korrektheit von Kalkülen zu zeigen.

Dafür muss man wissen, wie die Inferenzregeln sich verhalten zur Bedeutung.

Das ist fast immer einfach. In der Aussagenlogik war das sehr einfach. Wann ist A und B wahr? Wenn A wahr ist und gleichzeitig und unabhängig davon B wahr ist.

Wann ist A oder B wahr? Auch nicht schwer. Wenn A war, ist oder B war und es ist wohl Schwäches.

Wenn wir, wie dann später hier, Regeln haben werden, die wir uns gleich noch ein bisschen näher angucken, wenn wir Regeln haben, die Substitution machen,

dann müssen wir in dem Korrektheitsbeweis sagen, wann immer dieses hier allgemeingültig ist, ist das auch allgemeingültig.

Wir müssen irgendetwas über Bedeutung von A nach Substitution wissen. Und das ist gar nicht so ganz einfach.